Petri nets are a kind of formal language that are widely applied in concurrent systems associated with resource allocation due to their abilities of the natural description on resource allocation and the precise characterization on deadlock. Weighted System of Simple Sequential Processes with Resources (WS3PR) is an important subclass of Petri nets that can model many resource allocation systems in which 1) multiple processes may run in parallel and 2) each execution step of each process may use multiple units from a single resource type but cannot use multiple resource types. We first prove that the liveness problem of WS3PR is co-NP-hard on the basis of the partition problem. Furthermore, we present a necessary and sufficient condition for the liveness of WS3PR based on two new concepts called Structurally Circular Wait (SCW) and Blocking Marking (BM), i.e., a WS3PR is live iff each SCW has no BM. A sufficient condition is also proposed to guarantee that an SCW has no BM. Additionally, we show some advantages of using SCW to analyze the deadlock problem compared to other siphon-based ones, and discuss the relation between SCW and siphon. These results are valuable to the further research on the deadlock prevention or avoidance for WS3PR.

A Boolean network model is one of the models of gene regulatory networks, and is widely used in analysis and control. Although a Boolean network is a class of discrete-time nonlinear systems and expresses the synchronous behavior, it is important to consider the asynchronous behavior. In this paper, using a Petri net, a new modeling method of asynchronous Boolean networks with control inputs is proposed. Furthermore, the optimal control problem of Petri nets expressing asynchronous Boolean networks is formulated, and is reduced to an integer programming problem. The proposed approach will provide us one of the mathematical bases of control methods for gene regulatory networks.

A timed Petri net, an extended model of an ordinary Petri net with introduction of discrete time delay in firing activity, is practically useful in performance evaluation of real-time systems and so on. Unfortunately though, it is often too difficult to solve (efficiently) even most basic problems in timed Petri net theory. This motivates us to do research on analyzing complexity of Petri net problems and on designing efficient and/or heuristic algorithms. The minimum initial marking problem of timed Petri nets (TPMIM) is defined as follows: “Given a timed Petri net, a firing count vector X and a nonnegative integer π, find a minimum initial marking (an initial marking with the minimum total token number) among those initial ones M each of which satisfies that there is a firing scheduling which is legal on M with respect to X and whose completion time is no more than π, and, if any, find such a firing scheduling.” In a production system like factory automation, economical distribution of initial resources, from which a schedule of job-processings is executable, can be formulated as TPMIM. The subject of the paper is to propose two pseudo-polynomial time algorithms TPM and TMDLO for TPMIM, and to evaluate them by means of computer experiment. Each of the two algorithms finds an initial marking and a firing sequence by means of algorithms for MIM (the initial marking problem for non-timed Petri nets), and then converts it to a firing scheduling of a given timed Petri net. It is shown through our computer experiments that TPM has highest capability among our implemented algorithms including TPM and TMDLO.

In our privious paper, we proposed an algorithm that determines delay times of a timed Petri net from the structural information of a signaling pathway, but Petri net structures containing cycles and inhibitory arcs were not considered. This paper provides conditions for cycle-contained Petri nets to have reasonable delay times. Furthermore, handling of inhibitory arcs are discussed in terms of the reaction rate of inhibitory interaction in signaling pathway, especially the conversion process of Petri net with inhibitory arc to the one without inhibitory arc is given.

There are various existing methods translating timed Petri nets to timed automata. However, there is a trade-off between the amount of description and the size of state space. The amount of description and the size of state space affect the feasibility of modeling and analysis like model checking. In this paper, we propose a new translation method from timed Petri nets to timed automata. Our method translates from a timed Petri net to an automaton with the following features: (i) The number of location is 1; (ii) Each edge represents the firing of transition; (iii) Each state implemented as clocks and variables represents a state of the timed Petri net one-to-one correspondingly. Through these features, the amount of description is linear order and the size of state space is the same order as that of the Petri net. We applied our method to three Petri net models of signaling pathways and compared our method with existing methods from the view points of the amount of description and the size of state space. And the comparison results show that our method keeps a good balance between the amount of description and the size of state space. These results also show that our method is effective when checking properties of timed Petri nets.

Many Petri nets-based methods have been developed and applied to analyze cryptographic protocols. Most of them offer the analysis of one attack trace only. Only a few of them provide the analysis of multiple attack traces, but they are rather inefficient. Similarly, the limitation of the analysis of one attack trace occurs in most model checking methods for cryptographic protocols. Recently, we proposed a simple but practical Petri nets-based model checking methodology for the analysis of cryptographic protocols, which offers an efficient analysis of all attack traces. In our previous analysis, we assume that the underlying cryptographic algorithms are black boxes, and attackers cannot learn anything from cipher text if they do not have a correct key. In this paper, we relax this assumption by considering some algebraic properties of the underlying encryption algorithm. Then, we apply our new method to TMN authenticated key exchange protocol as a case study. Surprisingly, we obtain a very efficient analysis when the numbers of attack traces and states are large, and we discover two new attacks which exploit the algebraic properties of the encryption.

Petri net is a powerful modeling tool for concurrent systems. Subclasses of Petri net are suggested to model certain realistic applications with less computational cost. Structurally weakly persistent net (SWPN) is one of such subclasses where liveness is verified in deterministic polynomial time. This paper studies the computational complexity to verify whether a give net is SWPN. 3UNSAT problem is reduced to the problem to verify whether a net is not SWPN. This implies co-NP completeness of verification problem of SWPN.

The marking construction problem (MCP) of Petri nets is defined as follows: “Given a Petri net N, an initial marking Mi and a target marking Mt, construct a marking that is closest to Mt among those which can be reached from Mi by firing transitions.” MCP includes the well-known marking reachability problem of Petri nets. MCP is known to be NP-hard, and we propose two schemas of heuristic algorithms: (i) not using any algorithm for the maximum legal firing sequence problem (MAX LFS) or (ii) using an algorithm for MAX LFS. Moreover, this paper proposes four pseudo-polynomial time algorithms: MCG and MCA for (i), and MCHFk and MC_feideq_a for (ii), where MCA (MC_feideq_a, respectively) is an improved version of MCG (MCHFk). Their performance is evaluated through results of computing experiment.

This paper proposes a method to incorporate the concept of time for the inclusion of dynamics of signaling pathway in a Petri net model, i.e., to use timed Petri nets. Incorporation of delay times into a Petri net model makes it possible to conduct quantitative evaluation on a target signaling pathway. However, experimental data describing detailed reactions are not available in most cases. An algorithm given in this paper determines delay times of a timed Petri net only from the structural information of it. The suitability of this algorithm has been confirmed by the results of an application to the IL-1 signaling pathway.

Interrupt service routines are a key technology for embedded systems. In this paper, we introduce the standard approach for using Generalized Stochastic Petri Nets (GSPNs) as a high-level model for generating CTMC Continuous-Time Markov Chains (CTMCs) and then use Markov Reward Models (MRMs) to compute the performance for embedded systems. This framework is employed to analyze two embedded controllers with low cost and high performance, ARM7 and Cortex-M3. Cortex-M3 is designed with a tail-chaining mechanism to improve the performance of ARM7 when a nested interrupt occurs on an embedded controller. The Platform Independent Petri net Editor 2 (PIPE2) tool is used to model and evaluate the controllers in terms of power consumption and interrupt overhead performance. Using numerical results, in spite of the power consumption or interrupt overhead, Cortex-M3 performs better than ARM7.

Petri net is a powerful modeling tool for concurrent systems. Liveness, which is a problem to verify there exists no local deadlock, is one of the most important properties of Petri net to analyze. Computational complexity of liveness of a general Petri net is deterministic exponential space. Liveness is studied for subclasses of Petri nets to obtain necessary and sufficient conditions that need less computational cost. These are mainly done using a subset of places called siphons. CS-property, which denotes that every siphon has token(s) in every reachable marking, in one of key properties in liveness analysis. On the other hand, normal Petri net is a subclass of Petri net whose reachability set can be effectively calculated. This paper studies computational complexity of liveness problem of normal Petri nets. First, it is shown that liveness of a normal Petri net is equivalent to cs-property. Then we show this problem is co-NP complete by deriving a nondeterministic algorithm for non-liveness which is similar to the algorithm for liveness suggested by Howell et al. Lastly, we study structural feature of bounded Petri net where liveness and cs-property are equivalent. From this consideration, liveness problem of bounded normal Petri net is shown to be deterministic polynomial time complexity.

Invariants of Petri nets are fundamental algebraic characteristics of Petri nets, and are used in various situations, such as checking (as necessity of) liveness, boundedness, periodicity and so on. Any given Petri net N has two kinds of invariants: a P-invariant is a |P|-dimensional vector Y with Yt A = and a T-invariant is a |T|-dimensional vector X with A X = for the place-transition incidence matrix A of N. T-invariants are nonnegative integer vectors, while this is not always the case with P-invariants. This paper deals only with nonnegative integer invariants (invariants that are nonnegative vectors) and shows results common to the two invariants. For simplicity of discussion, only P-invariants are treated. The Fourier-Motzkin method is well-known for computing all minimal support integer invariants. This method, however, has a critical deficiency such that, even if a given Perti net N has any invariant, it is likely that no invariants are obtained because of an overflow in storing intermediate vectors as candidates for invariants. The subject of the paper is to give an overview and results known to us for efficiently computing minimal-support nonnegative integer invariants of a given Petri net by means of the Fourier-Motzkin method. Also included are algorithms for efficiently extracting siphon-traps of a Petri net.

The minimum initial marking problem of Petri nets (MIM) is defined as follows: "Given a Petri net and a firing count vector X, find an initial marking M0, with the minimum total token number, for which there is a sequence δ of transitions such that each transition t appears exactly X(t) times in δ, the first transition is enabled at M0 and the rest can be fired one by one subsequently." In a production system like factory automation, economical distribution of initial resources, from which a schedule of job-processings is executable, can be formulated as MIM. AAD is known to produce best solutions among existing algorithms. Although solutions by AMIM+ is worse than those by AAD, it is known that AMIM+ is very fast. This paper proposes new heuristic algorithms AADO and AMDLO, improved versions of existing algorithms AAD and AMIM+, respectively. Sharpness of solutions or short CPU time is the main target of AADO or AMDLO, respectively. It is shown, based on computing experiment, that the average total number of tokens in initial markings by AADO is about 5.15% less than that by AAD, and the average CPU time by AADO is about 17.3% of that by AAD. AMDLO produces solutions that are slightly worse than those by AAD, while they are about 10.4% better than those by AMIM+. Although CPU time of AMDLO is about 180 times that of AMIM+, it is still fast: average CPU time of AMDLO is about 2.33% of that of AAD. Generally it is observed that solutions get worse as the sizes of input instances increase, and this is the case with AAD and AMIM+. This undesirable tendency is greatly improved in AADO and AMDLO.

Communication-free Petri nets provide a net semantics for Basic Parallel Processes, which form a subclass of Milner's Calculus of Communicating Systems (CCS) a process calculus for the description and algebraic manipulation of concurrent communicating systems. It is known that the reachability problem for communication-free Petri nets is NP-complete. Lacking the synchronization mechanism, the expressive power of communication-free Petri nets is somewhat limited. It is therefore importance to see whether the power of communication-free Petri nets can be enhanced without sacrificing their analytical capabilities. As a first step towards this line of research, in this paper our main concern is to investigate, from the decidability/complexity viewpoint, the reachability problem for a number of variants of communication-free Petri nets, including communication-free Petri nets augmented with 'static priorities,' 'dynamic priorities,' 'states,' 'inhibitor arcs,' and 'timing constraints.'

The objective of this paper is to analyze a pull type multi-product, multi-line and multi-stage flexible manufacturing system whose resources are subject to planned and unplanned breakdown conditions. To ensure a continual supply of the finished products, under breakdown conditions, parts/materials flow through alternate routes exhibiting routing flexibility. The machine resources are flexible in this study and are capable of producing more than one item. Every machining and assembly station has been equipped with automated inspection units to ensure the quality of the products. The system is modelled through coloured Petri net methodology and the impact of input factors have been shown on the performance of the system. The study has been extended to explore near-optimal conditions of the system using design of experiment and response surface methods.

Petri nets are known as a modeling language for concurrent and distributed systems. In recent years, various object-oriented Petri nets were proposed, and we are proposing a kind of object-oriented Petri nets, called multi agent nets (MANs). In this letter, we consider the reachability analysis of MANs. We propose an algorithm for generating an abstract state space of a multi agent net, and report results of computational experiments.

This paper deals with WF-net based modeling and verification of interorganizational workflows (interworkflows for short) based on the protocol of WfMC. In the protocol, there are three patterns of interoperability: Chained, Nested, and Parallel synchronized; and an interworkflow is constructed by using those interoperability patterns. We first give a WF-net based modeling method. In this modeling method, the three interoperability patterns are respectively expressed in terms of WF-nets. They enable us to model a given interworkflow as a WF-net by connecting WF-nets representing its constituent workflows. We also indicate that if free choice WF-nets are connected by means of any combination of the three patterns then the resultant WF-net is asymmetric choice. Next we discuss verification of WF-nets obtained through the modeling method. Intuitively, a WF-net is said to be sound if, for any case, the initial state is always transformed to the final state. Unfortunately, even if every constituent WF-net is sound FC, the resultant WF-net is not always sound. We give a sufficient condition of non-soundness checkable in polynomial time. We also show that if they are connected by only the Nested pattern then the resultant WF-net is sound.

Petri nets with inhibitor arcs are referred to as inhibitor-arc Petri nets. It is shown that modeling capability of inhibitor-arc Petri nets is equivalent to that of Turing machines. The subject of this paper is the legal firing sequence problem (INLFS) for inhibitor-arc Petri nets: given an inhibitor-arc Petri net IN, an initial marking M0 and a firing count vector X, find a firing sequence δ such that its firing starts from M0 and each transition t appears in δ exactly X(t) times as prescribed by X. The paper is the first step of research for time complexity analysis and designing algorithms of INLFS, one of the most fundamental problems for inhibitor-arc Petri nets having more modeling capability than ordinary Peri nets. The recognition version of INLFS, denoted as RINLFS, means a decision problem, asking a "yes" or "no" answer on the existence of a solution δ to INLFS. The main results are the following (1) and (2). (1) Proving (1-1) and (1-2) when the underlying Petri net of IN is an unweighted state machine: (1-1) INLFS can be solved in pseudo-polynomial (O(|X|)) time for IN of non-adjacent type having only one special place called a rivet; (1-2) RINLFS is NP-hard for IN with at least three rivets; (2) Proving that RINLFS for IN whose underlying Petri net is unweighted and forward conflict-free is NP-hard. Heuristic algorithms for solving INLFS are going to be proposed in separate papers.

This paper considers Cyclic Job-Shop Scheduling Problems (CJSSP) extended from the Job-Shop Scheduling Problem (JSSP). We propose an evolutionary computing method to solve the problem approximately by generating the Petri net structure for scheduling. The crossover proposed in this paper employs structural analysis of Petri net model, that is, the crossover improves the cycle time by breaking the bottle-neck circuit obtained by solving a linear programming problem. Experimental evaluation shows the effectiveness of our approach.

Petri nets have recently become widely accepted as a description method for biological pathways by researchers in computer science as well as those in biology. This paper gives an overview of Petri net formalisms to describe biological pathways and discusses their use in modelings and simulations for the systematic understandings of biological pathways. After reviewing the use of various types of Petri nets for the biological pathway modelings, we showed the examples that analyze fundamental properties of biological pathways using T-invariant, P-invariant, siphon, and trap. Applications of hybrid Petri nets for producing new biological hypotheses through simulations are also illustrated.